This invention relates to a method for deriving a functional circuit description from a structural circuit description, containing pre-charge logic, dependent upon pre-charge node values. The functional circuit description is independent of pre-charge node values. Accordingly, the invention is particularly useful for, but not necessarily limited to, translating the initial circuit description into a higher level behavioural circuit description that is independent of pre-charge node values.
Contemporary chip design depends critically on the availability of appropriate CAD tools in order to keep up with the ever increasing chip complexity. Designers typically work with chip descriptions at several levels of abstraction. The Register-Transfer Level (RTL) describes a circuit at the high level of Boolean functions and data flow within the circuit much like a regular programming language does. Gate-level descriptions provide a structural (schematic) description of a circuit as an interconnection of gates having a known and relatively simple Boolean behaviour. Switch-level descriptions represent the lowest level of circuit design abstraction. Switch-level descriptions are also structural (schematic) and contain an interconnection of switches (transistors) that implement the desired functionality of the circuit.
The RTL is often the preferred abstraction level for most design activities, however, any RTL design has to be translated into an equivalent switch-level design as a necessary step prior to chip fabrication. This translation can be performed using synthesis Electronic Design Automation (EDA) tools that compile RTL designs into a predefined technology-specific gate-level cell library containing a switch-level schematic for each cell. In some cases, especially when a chip has to meet stringent operating requirements (speed, power consumption, etc.), certain blocks of the chip may be designed at the switch level.
For a number of reasons, it is highly desirable and advantageous to accurately translate the functionality implemented by a circuit description containing switches into a higher level (gate or RTL). This is useful for formal functional verification to ensure that a chip operates as expected based on appropriate mathematical models. Unlike traditional functional verification approaches, such as simulation, formal verification provides 100% coverage of a circuit""s functionality. To enable formal functional verification at a mixed (switch and gate) level, a method is required to translate the structural description of a circuit into a functional (Boolean) description in the corresponding mathematical model. Other application areas for mixed (switch and gate) level circuit analysis and translation include technology-specific library characterization, Automatic Test Pattern Generation (ATPG), and re-synthesis and re-design of chips from one chip manufacturing technology to another.
A family of mixed (switch and gate) level structures that utilise pre-charge logic (including dynamic, domino and non-footed pre-charge logic and various pre-charge clock tree and level restoring logic schemes) are particular difficult to analyse. Such circuits exploit their inherent dynamic characteristics in order to simultaneously increase operational speed and reduce circuit power consumption. The unique features of pre-charge logic circuits include a dependence on pre-charge clock inputs and a reliance on some form of net capacitance or level restoring logic at certain nodes in the circuit, named pre-charge nodes.
One aspect in deriving a functional model of a mixed (switch and gate) level circuit is the ability to identify and properly characterise the behaviour induced at pre-charge nodes by the introduction of pre-charge clock inputs. Various techniques have been developed for the analysis of the behaviour of mixed (switch and gate) level circuits. However, these techniques are based on a static switch-level model that ignores pre-charge clock inputs and the consequent dynamic or transient signal behaviour at pre-charge nodes. Therefore, they are unable to automatically model the dynamic behaviour at pre-charge nodes or subsequently produce an accurate functional description of that behaviour.
Tools known as ANAMOS and TRANALYZE, described in xe2x80x9cBoolean Analysis of MOS Circuitsxe2x80x9d by R. E. Bryant published in IEEE TCAD, 6(4), pp. 634-649, July 1987, and later refined in xe2x80x9cExtraction of Gate-Level Models from Transistor Circuits by Four-Valued Symbolic Analysisxe2x80x9d also by R. E. Bryant and published in ICCAD ""91, do not give special treatment to pre-charge clock inputs or pre-charge nodes. The ANAMOS and TRANALYZE tools were developed for transistor-level simulation and mapping into a hardware-based gate-level simulator. These tools use dynamic behaviour at pre-charge nodes is modelled during the simulation step rather than during transistor-level extraction.
Another approach to mixed (gate and switch) level circuit analysis has been implemented in a tool developed by International Business Machines Corporation. This tool is described in xe2x80x9cVerityxe2x80x94a Formal Verification Program for Custom CMOS Circuitsxe2x80x9d by A. Kuehlmann, A. Srinivasan and D. P. LaPotin published in the IBM R and D Journal, Vol. 39, pp. 149-165, Januaryxe2x80x94March 1995. This tool is a logic checker working at the switch level. The tool does not provide an equivalent higher-level model. It does give special treatment to pre-charge nodes, however the technique requires the user to specify the location of all pre-charge nodes to the tool.
In this specification, including the claims, the terms xe2x80x9ccomprisesxe2x80x9d, xe2x80x9ccomprisingxe2x80x9d or similar terms are intended to mean a non-exclusive inclusion, such that a method or apparatus that comprises a list of elements does not include those elements solely, but may well include other elements not listed.
According to one aspect of the invention there is provided a method for deriving a functional circuit description that is independent of pre-charge node values, the functional circuit description being a transformation of an initial structural circuit description having pre-chargeable nodes, the method comprising the steps of:
identifying said pre-chargeable nodes in said initial structural circuit description, said pre-chargeable nodes having a logic value that is dependent upon an associated pre-charge clock;
determining said pre-charge node values associated with said pre-chargeable nodes;
deriving said functional circuit description that is independent of pre-charge node values.
Suitably, after the step of deriving, there may be a further step of translating the said functional circuit description into a hardware description language representation.
Suitably, the step of translating may include the step of applying a constant logic value to each internal pre-charge clock in the transformed circuit description.
Preferably, the step of translating may include the step of providing the pre-charge clock as part of the hardware description language representation.
Suitably, the step of identifying may be effected automatically.
Preferably, the step of identifying may include identifying nodes that are floating during part of a pre-charge clock cycle, these nodes being pre-charge nodes.
Suitably, the step of determining may include heuristic assessment of logic pull up and logic pull down conditions associated with each pre-charge node.